Issue402.agda:13,12-16
x != y of type Unit
when checking that the expression refl has type x == y
